\documentclass{beamer}

%% comente a linha acima e descomente a debaixo para gerar
%% l minas para serem impressas
% \documentclass[handout]{beamer}

% Outras classes: [notes], [notes=only], [trans], [handout],
% [red], [compress], [draft], [class=article]
\usetheme{Antibes} % Beamer theme v 3.0
%\usecolortheme{lily}

\mode<presentation>{
  %% Temas
%  \usepackage{beamerthemeshadow}
%	\usepackage{beamerwarsaw}
  \usepackage{beamerthemeMadrid}
% 	\usepackage{beamerthemeHannover}

%   \usepackage[headheight=12pt,footheight=12pt]{beamerthemeboxes}
%   \usepackage{beamerthemeclassic}
%   \usepackage{beamerthemelined}
%   \usepackage{beamerthemeplain}
%   \usepackage[width=12pt,dark,tab]{beamerthemesidebar}
%   \usepackage{beamerthemesplit}
%   \usepackage{beamerthemetree}
%   \usepackage[bar]{beamerthemetree}

\usepackage{hyperref}  % faz funcionar o \hipersetup

\hypersetup{colorlinks,
   debug=false,
   pdfpagemode=FullScreen,
   linkcolor=black,  %%% cor do tableofcontents, \ref, \footnote, etc
   citecolor=red,  %%% cor do \cite
   urlcolor=blue,   %%% cor do \url e \href
   bookmarksopen=true,
   pdftitle={...},
   pdfauthor={},
   pdfsubject={LaTeX},
   pdfkeywords={LaTeX}
}
 
  \usepackage{pgf,pgfarrows,pgfnodes,pgfautomata,pgfheaps,pgfshade}
  \beamertemplatetransparentcovereddynamic
  \beamertemplateballitem
  % \beamertemplatefootpagenumber
}

\mode<handout>{
  % tema simples para ser impresso
  \usepackage[bar]{beamerthemetree}
  % Colocando um fundo cinza quando for gerar transpar ncias para serem impressas
  % mais de uma transpar ncia por p gina
  \beamertemplatesolidbackgroundcolor{black!5}
}


\usepackage{multirow}
\usepackage{amsmath,amssymb,amsfonts}
\usepackage{multicol,ragged2e}
\usepackage{hyphenat}
\usepackage{setspace}
\usepackage{times}
%\usepackage{indentfirst}
%\usepackage{setspace}
\usepackage[utf8]{inputenc}
\usepackage[brazil]{babel}
\usepackage{graphicx,url}
\usepackage{subfigure}
\usepackage{longtable}
\usepackage{ctable}
\usepackage{graphicx}
% Muda o estilo do caption de figuras e tabelas para serem numerados - ALELUIA - não aguentava mais aquelas figuras sem numero das apresentações latex :-)
\setbeamertemplate{caption}[numbered]

% Cor da apresentação ------------
% \usepackage{colortbl}
% \usepackage{beamercolorthemeseahorse}
% \usepackage{beamercolorthemewhale}
% \usepackage{beamercolorthemesidebartab}
% \usepackage{beamercolorthemebeetle}
% \usepackage{beamercolorthemelily}
 \usepackage{beamercolorthemedove}
% \usepackage{beamercolorthemealbatross}

% um outro tipo de fonte ---------
% \usepackage{pslatex}

\newcommand{\topic}{
       \vfill \item
}

\beamertemplatetransparentcovereddynamic

\title[Verificação Automática]{Low-Power Design Applications for Formal Verification \\ Author: \textit{Saptarshi Biswas} \\ Contributor:  Jasper Design Automation}
\author[Oliveira]{Rangel Silva Oliveira\inst{1}}
	\institute[DCC/UFMG]{
		\inst{1}
		Universidade Federal de Minas Gerais\\
		Departamento de Ciência da Computação\\
	}

	
\date{\today}
%\pgfdeclareimage[height=1.0cm]{logo}{figuras/Logo_lapo}
%\logo{\pgfuseimage{logo}}

\begin{document}
\newcommand{\goodgap}{%
                                                       \hspace{\subfigtopskip}%
                    \hspace{\subfigbottomskip}}

\frame{
	\titlepage
}
\frame{
	\frametitle{Sumário}	
\tableofcontents
}
	
	\AtBeginSection[]{
 		\frame<handout:0>{
 			\frametitle{Sumário}
 			\tableofcontents[current,currentsection]
 		}
 	}

	\AtBeginSubsection[]{
		\frame<handout:0>{
			\frametitle{Sumário}
			\tableofcontents[current, currentsection, currentsubsection]
		}
	}

\section{Introdução}
\frame{
	\frametitle{Introdução}
	\begin{itemize}
		\topic<1-| alert@1> Dispositivos móveis: durabilidade de suas baterias, complexidade dos hardware atuais;
		\topic<2-| alert@2> Técnicas avançadas para eficiência no consumo de energia;
	  \topic<3-| alert@3> Incremento da complexidade dos seus projetos;
		\topic<4-| alert@4> Complexidade dos chips em relação aos domínios de potência fazem da verificação uma tarefa difícil;
		\topic<5-| alert@5> Verificação formal é essencial para lidar com essas complexidades e obter uma confiança máxima de verificação.
		\vfill
	\end{itemize}
}


\section{Complexidade da verificação: Low-power design}
\frame{
	\frametitle{Complexidade da verificação: \textit{Low-power} design}
		\begin{itemize}
		\topic<1-| alert@1> Os esquemas de hardware estão se tornando mais complexos devido ao elevado grau de integração do sistema;
		\topic<2-| alert@2> O número de modos de operação devido às funções de gerenciamento de energia estão aumentando;
		\topic<3-| alert@3> Os projetos tem domínios complexos de energia, organizados de forma aninhada e hierárquica.
		\vfill
	\end{itemize}
}

\frame{
	\frametitle{Complexidade da verificação: \textit{Low-power} design}
	\begin{center}
	  \begin{figure}
	  \includegraphics[scale=0.50]{Jasper-05-07-10-Fig1.jpg}
	  \caption{Diagrama de Bloco de um \textit{Smartphone}}
	  \end{figure}
  \end{center}
  
  A verificação deve garantir que todos esses componentes trabalhem em conjunto de forma confiável em todos os momentos.

}


\frame{
	\frametitle{Complexidade da verificação: \textit{Low-power} design}
	\begin{itemize}
			\topic<1-| alert@1> Um chip pode ter vários modos de operação;
			\topic<2-| alert@2> Incremento da demanda por energia nos dispositivos;
			\topic<3-| alert@3> Adição de múltiplos modos de operação;
			\topic<4-| alert@4> Segurança de economia de energia quando certos blocos funcionais não forem necessários.
		\vfill
	\end{itemize}
}


\frame{
	\frametitle{Complexidade da verificação: \textit{Low-power} design}
	\begin{center}
	  \begin{figure}
	  \includegraphics[scale=0.65]{Jasper-05-07-10-Fig2.png}
	  \caption{Domínios e modos de potência para o chip de um \textit{Smartphone}}
	  \end{figure}
  \end{center}
}

\frame{
	\frametitle{Complexidade da verificação: \textit{Low-power} design}
		\begin{itemize}
			\topic<1-| alert@1> Domínios de potência são também construídos hierarquicamente;
			\topic<2-| alert@2> Eles podem residir dentro de outros domínios de potência;
			\topic<3-| alert@3> O dispositivo pode ser totalmente controlado a partir do primeiro nível do domínio de potência;
			\topic<4-| alert@4> Curiosidade: complexidade de verificação de um processador i7 rodando \textit{iTunes}.
		\vfill
	\end{itemize}
}

\frame{
	\frametitle{Complexidade da verificação: \textit{Low-power} design}
	
\begin{center}
	  \begin{figure}
	  \includegraphics[scale=0.50]{Jasper-05-07-10-Fig3.jpg}
	  \caption{Domínio de potência hierárquico com dependências}
	  \end{figure}
  \end{center}
}

\frame{
  \frametitle{Complexidade da verificação: \textit{Low-power} design}
	\begin{block}{Exemplo: os domínios de potência são definidos como:}
	\begin{itemize}
		\topic<1-| alert@1> Processador principal;
		\topic<1-| alert@1> Unidade de transmissão;
		\topic<1-| alert@1> Unidade de \textit{display};
		\topic<1-| alert@1> Unidade de processamento de imagem;
		\topic<1-| alert@1> e o resto.
	\end{itemize}
	\end{block}	
	
}

\frame{
  \frametitle{Complexidade da verificação: \textit{Low-power} design}
\begin{block}{Os 9 diferentes modos para o chip acima são resumidos como se segue:}
\begin{itemize}
		\topic<1-| alert@1> Modo funcional ao máximo, onde todos os domínios de potência estão ligados e funcionando na tensão máxima;
		\topic<2-| alert@2> Um modo texto, onde o processamento de imagens e o resto estão chaveados para baixa tensão;
		\topic<3-| alert@3> Um modo telefone, onde o bloco de transmissão está totalmente ligado;
		\topic<4-| alert@4> Um modo de acesso \textit{PIM}, onde a unidade de processamento de imagens está desligado.
		\vfill
	\end{itemize}
	\end{block}
}


\frame{
	\frametitle{Complexidade da verificação: \textit{Low-power} design}
\begin{block}{Os 9 diferentes modos para o chip acima são resumidos como se segue:}	
	\begin{itemize}
		\topic<1-| alert@1> Modo Câmera, quando as unidade de processamento de imagens e \textit{display} estão ligados;
		\topic<2-| alert@2> Modo de reprodução, quando a unidade de \textit{display} está totalmente ligada;
		\topic<3-| alert@3> Modo de jogos, quando as unidades do processador e do \textit{display} estão ligados;
		\topic<4-| alert@4> Modo \textit{keep-alive}, quando o processador está ligado e a unidade de transmissão está em baixa tensão;
    \topic<5-| alert@5> Modo desligado, quando tudo está desligado.
	\end{itemize}
	\end{block}
}

\frame{
	\frametitle{Complexidade da verificação: \textit{Low-power} design}
	\begin{itemize}
		\topic<1-| alert@1> Funções de gerenciamento de potência dentro de um único bloco funcional chamado: \textit{power management unit (PMU)};
		\topic<2-| alert@2> Os \textit{PMU} controlam os sinais e a lógica sequencial associada, controlando e sequenciando todos os domínios de potência.
	\end{itemize}
}

\section{Verificação Formal para projetos de baixa potência}
\frame{
	\frametitle{Verificação Formal para projetos de baixa potência}
	\begin{itemize}
		\topic<1-| alert@1> Uma \textit{PMU} implementa a arquitetura de baixa potência para um chip;
		\topic<2-| alert@2> Ao projetar a \textit{PMU}, duas decisões deve ser tomadas: quais técnicas de potência usar e como particionar o projeto;
		\topic<3-| alert@3> Consumo total de energia do \textit{chip}: potência média, instantânea e o pior cenário possível;
		\topic<4-| alert@4> Verificação Formal: encontrar o caso em que os sinais alternam mais ou menos no \textit{chip};
		\topic<5-| alert@5> Técnicas de controle de potência em qualquer projeto: \textit{clock gating, power shut-down (power gating), voltage scaling}.
	\end{itemize}
}


\section{Mecanismos de falha em projetos de baixa potência}
\frame{
	\frametitle{Mecanismos de falha em projetos de baixa potência}
\begin{block}{Falhas estruturais}
		\begin{itemize}
		\topic<1-| alert@1> Para verificar o projeto em busca de falhas estruturais, todo o projeto precisa ser analisado.
    \topic<2-| alert@2> Podem ser detectados estaticamente através de uma análise do fluxo do esquema lógico.
    \topic<3-| alert@3> Estão relacionadas a falhas de implementação dos projetistas.
\end{itemize}
\end{block}
}

\frame{
	\frametitle{Mecanismos de falha em projetos de baixa potência}
	
	\begin{itemize}
		\topic<1-| alert@1> Falhas temporais são causadas por sequencia incorreta de sinais de controle emitidos pela \textit{PMU};
		\topic<2-| alert@2> Erros de interação de \textit{Clock}:
		 \vfill	
	\begin{center}
	  \begin{figure}
	  \includegraphics[scale=0.50]{Jasper-05-07-10-Fig4.png}
	  \caption{Nesse exemplo, o \textit{clock} pode ser parado quando o dado está no Estágio 2. A restauração do \textit{clock} sem considerar o tempo de permanência do Estágio 2 pode resultar em dado corrompido}
	  \end{figure}
  \end{center}
\topic<3-| alert@3> Erros de estado de potência;
\topic<4-| alert@4> Erros de tempos de habilitação.
	\end{itemize}
}

\frame{
	\frametitle{Mecanismos de falha em projetos de baixa potência}
	\begin{itemize}
		\topic<1-| alert@1>	Erros de sequencia\vfill
		\vfill
	\begin{center}
	  \begin{figure}
	  \includegraphics[scale=0.70]{Jasper-05-07-10-Fig5.png}
	  \caption{Exemplos de erros de sequencia}
	  \end{figure}
  \end{center}
  \vfill
  \topic<2-| alert@2> Erros de ordenação de domínios: sinal de controle de um domínio de alta ordem passando por um de baixa ordem.
  	\end{itemize}
}



\frame{
	\frametitle{Mecanismos de falha em projetos de baixa potência: Erros de conservação de estados}
	\begin{center}
	  \begin{figure}	
	  \includegraphics[scale=0.60]{Jasper-05-07-10-Fig6.png}
	  \caption{Registrador do estado de conservação e a sequencia}
 	  \end{figure}
  \end{center}
}

\section{Completando a verificação de projetos de baixa potência}

\frame{
	\frametitle{Completando a verificação de projetos de baixa potência}
	\textbf{Verificação Formal:} verifica projetos de baixa potência contra essas falhas funcionais
	\begin{center}
	  \begin{figure}
	  \includegraphics[scale=0.50]{Jasper-05-07-10-Fig7.png}
	  \caption{Exemplo de um projeto de baixa potência com alta complexidade de verificação}
	  \end{figure}	
  \end{center}
}


\frame{
	\frametitle{Completando a verificação de projetos de baixa potência}
	\begin{center}
	  \begin{figure}
	  \includegraphics[scale=0.65]{Jasper-05-07-10-Table1.png}
	  \caption{Tabela de estados para o exemplo de projeto}
	  \end{figure}
  \end{center}
}

\frame{
	\frametitle{Completando a verificação de projetos de baixa potência}
	\begin{center}
	  \begin{figure}
	  \includegraphics[scale=0.50]{Jasper-05-07-10-Fig8.png}
	  \caption{Grafo de ordenação de domínio para o projeto. Domínio A e C não são relacionados, sendo assim, nenhuma verificação é necessária}
	  \end{figure}
  \end{center}
}

\frame{
	\frametitle{Completando a verificação de projetos de baixa potência}
	\begin{center}
	  \begin{figure}
	  \includegraphics[scale=0.50]{Jasper-05-07-10-Fig9a.jpg}
	  \caption{Checagem temporal para o projeto de exemplo}
	  \end{figure}
  \end{center}
}

\section{Conclusão}
\frame{
	\frametitle{Conclusão}
  \begin{itemize}
		\topic<1-| alert@1> Verificação Formal está emergindo como uma solução apropriada para verificar muitos aspectos de projetos de baixo consumo;
	\topic<2-| alert@2> Falhas em projetos de baixo consumo: complexidade inerente entre as interações com múltiplos modos de potência para diminuir o consumo de energia;
	\topic<3-| alert@3> Projetistas usam a simulação para verificar se todos os erros foram identificados e corrigidos;
		\vfill
	\end{itemize}
}

\frame{
	\frametitle{Conclusão}
  \begin{itemize}
	\topic<1-| alert@1>	Verificação Formal: completa verificação e validação exaustiva da \textit{PMU};
	\topic<2-| alert@2> Técnicas de Verificação Formal são melhores que simulação para erros temporais;
	\topic<3-| alert@3> Elas verificam a classe de erros inteira em apenas algumas checagens;
	\topic<4-| alert@4> Elas são exaustivas e encontram todos os erros no projeto, ao contrário da simulação.
		\vfill
	\end{itemize}
}
%------------------------------------------------------------------------- 
\section{Perguntas}
	\frame{
		\frametitle{Perguntas?}
    \begin{itemize}
      \item Contato: rangel@dcc.ufmg.br
    \end{itemize}
}

\section{Referências}
	\frame{
		\frametitle{Referências}
    \begin{itemize}
			\item Artigo disponível em: \\ 
		\href{http://www.soccentral.com/results.asp?CatID=488&EntryID=31280}{http://www.soccentral.com}. 
		\end{itemize}
	}

\end{document}
